\begin{tabbing}
$\forall$\=${\it es}$:ES, $C$, $T$:Type, $R_{1}$, $R_{2}$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$), ${\it decodes}_{1}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R_{1}$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),\+
\\[0ex]${\it decodes}_{2}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R_{2}$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$).
\-\\[0ex]($\forall$$i$:$C$, $e$:E. Dec($R_{1}$($i$,$e$)))
\\[0ex]$\Rightarrow$ ($\forall$$i$:$C$, $e$:E. Dec($R_{2}$($i$,$e$)))
\\[0ex]$\Rightarrow$ ($\forall$$i$:$C$, $e$:E. $\neg$($R_{1}$($i$,$e$) \& $R_{2}$($i$,$e$)))
\\[0ex]$\Rightarrow$ ($\exists$\=${\it decodes}$:$i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ ($R_{1}$($i$,$x$)) $\vee$ ($R_{2}$($i$,$x$))\} $\rightarrow$state@loc($e$)$\rightarrow$$T$\+
\\[0ex]($\forall$$i$:$C$, $e$:\{$x$:E$\mid$ ($R_{1}$($i$,$x$)) $\vee$ ($R_{2}$($i$,$x$))\} , ${\it st}$:state@loc($e$).
\\[0ex](($R_{1}$($i$,$e$)) $\Rightarrow$ (${\it decodes}$($i$,$e$,${\it st}$) = ${\it decodes}_{1}$($i$,$e$,${\it st}$)))
\\[0ex]\& (($R_{2}$($i$,$e$)) $\Rightarrow$ (${\it decodes}$($i$,$e$,${\it st}$) = ${\it decodes}_{2}$($i$,$e$,${\it st}$)))))
\-
\end{tabbing}